perm filename ORDER.PRB[W79,JMC]1 blob sn#407320 filedate 1979-01-01 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Let the ordinals less than epsilon zero be represented as numbers
C00003 ENDMK
CāŠ—;
Let the ordinals less than epsilon zero be represented as numbers
and lists.  An ordinal is either a number or a list of ordinals
in descending order.  Write programs as follows:

1. To test whether an S-expression represents and ordinal.

2. To compare two ordinals.

Make proofs as follows:

1. Prove that the above written programs are total.

2. Prove trichotomy.

3. Prove transitivity.

Write a schema expressing the fact that the ordering is a well-ordering.

Can you prove it?